.TH YICES-SMT2 1 "June 2024" "Yices 2.6.5" "User Commands"
.SH NAME
yices-smt2 \- the Yices SMT solver for the SMT-LIB 2 language
.SH SYNOPSIS
.B yices-smt2
[
.I option
]
[
.I file
]
.SH DESCRIPTION
Runs the Yices SMT solver on an input problem written in SMT-LIB 2 language.
If no
.I file
is given, the problem is read from standard input.
.P
The SMT-LIB language and logical theories are documented at http://smtlib.cs.uiowa.edu.
.
.SH OPTIONS
.TP
.B \-\-version,  \-V
Display version and exit.
.TP
.B \-\-help,  \-h
Display a short help summary.
.TP
.BI \-\-verbosity= level, \& " "  \-v  "" " " level
Set the verbosity level (default = 0).
.TP
.BI \-\-timeout= timeout, \& "" \-t "" " " timeout
Give a
.I timeout
in seconds. There is no timeout by default.
.TP
.B \-\-stats,  \-s
Print a statistics summary before exiting.
.TP
.B \-\-incremental
Enable support for the push/pop commands.
.TP
.B \-\-interactive
Run in interactive mode.
.IP
This option is ignored if an input
.I file
is given on the command line. Otherwise,
.B yices-smt2
prints a prompt before every command. This also sets the SMT-LIB option
.I :print-success
to true.
.TP
.B \-\-mcsat
Force use of the MCSAT solver.
.TP
.B \-\-yices-model-format
Print models in the Yices model format (instead of the SMT-LIB format)..
.TP
.B \-\-bvconst-in-decimal
Print bitvector constants using the SMT-LIB decimal format, instead of the binary format.
.TP
.BI \-\-delegate= solver
Selects an third-party backend SAT solver for bit-vector problems.
.IP
The
.I solver
must be either
.I cadical
or
.I cryptominisat
or
.I y2sat.
This option has no effect unless the logic if QF_BV.
.TP
.BI \-\-dimacs= filename
Bit-blast then export the CNF to a file in the DIMACS format. This option is ignored unless
the logic is QF_BV.
.TP
.B \-\-mcsat-help
Display options used only by the MCSAT solver.
.SH SEE ALSO
.BR yices (1),
.BR yices-sat (1),
.BR yices-smt (1),
.PP
To report bugs and to get the full documentation, please visit http://yices.csl.sri.com.
.
.SH AUTHORS
.PP
Copyright (C) SRI International.
.PP
Yices is developed at SRI's Computer Science Laboratory. The main developers
are Bruno Dutertre <bruno@csl.sri.com>, Dejan Jovanovic <dejan@csl.sri.com>, Ian A. Mason <iam@csl.sri.com>,
and Stephane Graham-Lengrand <stephane.graham-lengrand@sri.com>.
